(declare-const a String)
(declare-const b String)
(declare-const c String)
(declare-const d String)
(assert (distinct c d))
(assert (= (str.++ a d b) (str.++ d c)))
(check-sat)
(declare-const a String)
(declare-const b String)
(declare-const c String)
(declare-const d String)
(assert (distinct c d))
(assert (= (str.++ a d b) (str.++ d c)))
(check-sat)
